/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import java.util.BitSet;

import alloy.util.Dbg;

/**
 * Represents a partial assignment to Boolean variables.  Each Boolean variable
 * is either true, false or unassigned.
 */
public class PartialAssignment {
    /** An empty partial assignment: one that assigns no variables. */
    public static PartialAssignment EMPTY_ASSIGNMENT = new PartialAssignment();
    
    public static void initSingleton() {
    	EMPTY_ASSIGNMENT = new PartialAssignment();
    }
    
    /** Which variables are assigned */
    private BitSet _assignedVars = new BitSet();

    /** Which variables are true */
    private BitSet _trueVars = new BitSet();

    /** Create an empty {@link PartialAssignment} in which all variables are unassigned */
    public PartialAssignment() { }

    /**
     * Create an {@link PartialAssignment} in which the variable i is assigned
     * the truth value from the i'th element of the given boolean[] (element 0
     * is unused).
     */
    public PartialAssignment(boolean[] assignment_) {
	for (int i=1; i<assignment_.length; i++)
	    setVarValue(i, assignment_[i]);
    }

    /** Set the value of a boolean variable */
    public void setVarValue(int var_, boolean val_) {
	_assignedVars.set(var_-1);
	if (val_)
	    _trueVars.set(var_-1);
	else
	    _trueVars.clear(var_-1);
    }

    /**
     * Get the value of a boolean variable {@link #isAssigned assigned}
     * by this partial assignment.
     */
    public boolean getVarValue(int var_) {
	Dbg.chk(isAssigned(var_));
	return _trueVars.get(var_-1);
    }
    
    /**
     * Get the value of a boolean <em>literal</em> {@link #isAssigned assigned}
     * by this partial assignment.
     */
    public boolean getLitValue(int lit_) {
	boolean varValue = getVarValue(Math.abs(lit_));
	return lit_ > 0 ? varValue : !varValue;
    }

    /**
     * Set the value of a boolean <em>literal</em> in this partial assignment.
     */
    public void setLitValue(int lit_, boolean litValue_) {
	int var = Math.abs(lit_);
	setVarValue(var, lit_ > 0 ? litValue_ : !litValue_);
    }

    /**
     * Return the highest-numbered Boolean variable assigned by this
     * partial assignment.
     */
    public int getMaxVar() { return _assignedVars.length()+1; }
    
    /**
     * Return a boolean[] where element 0 is unused and element i gives the boolean value
     * assigned to variable i.  Assumes that all variables are assigned. */
     public boolean[] toBoolArray() {
	 boolean[] result = new boolean[_assignedVars.length()+1];
	 for (int i=1; i<result.length; i++) {
	     result[i] = getVarValue(i);
	 }
	 return result;
     }
    
    /**
     * Test whether a given Boolean variable is assigned by this partial assignment.
     */
    public boolean isAssigned(int var_) { return _assignedVars.get(var_-1); }

    public String toString() { return "[assignedVars: " + _assignedVars + " trueVars: " + _trueVars + "]"; }
}  // class PartialAssignment
